Designing and fabricating electronic devices typically involves many steps, known as a “design flow.” The particular steps of a design flow often are dependent upon the type of circuitry, its complexity, the design team, and the device fabricator or foundry that will manufacture the electronic device. Typically, software and hardware “tools” verify the design at various stages of the design flow by running software simulators and/or hardware emulators, and errors in the design are corrected or the design is otherwise improved.
Several steps are common to most design flows for integrated microcircuits. Initially, the specification for a new circuit is transformed into a logical design, sometimes referred to as a register transfer level (RTL) description of the circuit. With this logical design, the circuit can be described in terms of both the exchange of signals between hardware registers and the logical operations that can be performed on those signals. The logical design typically employs a Hardware Design Language (HDL), such as the Very high speed integrated circuit Hardware Design Language (VHDL). At various stages of the design flow, the design is transformed into a different representation, for example, the transformation of the design from an RTL representation to a gate-level netlist representation during synthesis, the transformation of the gate-level netlist to a physical design layout, or the like. These transformations are intended to convert the design into an equivalent representation, albeit at a different level of abstraction than the previous representation of the design, which retains the functionality of the design. To help ensure that a transformation did not alter the functionality of the design, an equivalence of the different design representations can be determined, for example, using formal techniques provided by a Binary Decision Diagram (BDD) tool, a Satisfiability Prover (SAT) tool, an Automatic Test Pattern Generator (ATPG) tool, or the like. Typically, an equivalence checking tool utilizes a matching register hypothesis, which assumes that the different design representations each have combinational logic with the same functionality located between registers. This assumption of a 1-to-1 correspondence between registers in the different design representations, allows the equivalence checking tool to sub-divide the different design representations into combinational logic portions based on the locations of their registers and perform the formal techniques on those portions to determine whether they are equivalent.
Modern circuit design synthesis, however, often utilizes optimizations when converting one design representation into another design representation, which can invalidate the matched register hypothesis. For example, a synthesis engine can perform various timing optimizations that can move combinational logic in the synthesized design representation across a register boundary. The synthesis engine also can perform state minimization, state encoding, sequential-redundancy removal and addition, which can alter a structure of the design representations. Since this type of optimization renders the combinational logic located between registers different for the different design representations, the matched register hypothesis becomes invalid for that portion of the design representations.
Some equivalency checking engineers have attempted to cure the loss of the matched register hypothesis caused by the optimizations by altering the original design representation to recreate the 1-to-1 register matching between the designs. For example, these equivalency checking engineers often utilize a guidance file, which can describe the optimizations performed by a synthesis engine, to reconstruct the combinational logic optimizations in the original design representation in order to reestablish the matching register hypothesis. This approach, however, avails itself to many reconstruction flaws and eliminates independent analysis of whether the synthesis engine generated a design representation that is equivalent to the original design representation that was synthesized.
Another proposed technique to formally verify structurally transformed designs is referred to as sequential equivalence checking. Sequential equivalence checking traverses a state space of the two design representations prior to verification, often consuming significantly more computational resources than conventional formal verification techniques require. Since the state space increases exponentially with based on the size of the circuit design, it is often not feasible to formally utilize sequential techniques for equivalence checking.